A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method

摘要

The OTS/CafeOBJ method can be used to model, specify and verify distributed systems. Specifications are written in equations, which are regarded as rewrite rules and used to verify specifications. The usefulness of the method is demonstrated by applying the method to nontrivial problems such as electronic commerce protocols and railroad signaling systems. In this paper we describe a toolkit called Buffet, which assists verification in the method. Given predicates used to split cases and lemmas, Buffet automatically generates proofs (Called proof scores) and checks the proof scores using the CafeOBJ system. Buffet also has facilities to display proof scores generated and verification results on a web browser.